Inductive MatrixEval (s: State)(m n: Integer) : MatrixExp -> Matrix Byte m n -> Prop :=
  | matrix_eval_lit : forall (mx:Matrix Byte m n),
      MatrixEval s (matrix_exp_lit mx) mx
  
  | matrix_eval_id : forall (i:Id)(mx:Matrix Byte m n),
    s i = Some (byte_matrix_val mx) -> MatrixEval s (matrix_exp_id i) mx

  | matrix_eval_init : forall aexp1 aexp2 a,
                        ArithEval s aexp1 m -> ArithEval s aexp2 n ->
                        MatrixEval s (matrix_exp_init aexp1 aexp2) (matrix_zero a m n)
.